#ifndef TERN_SCHED_H
#define TERN_SCHED_H

#include <pthread.h>
#include <stdint.h>
#include <inttypes.h>
#include <string>

using namespace std;

namespace klee {
	// The abstract parent class for both memoizer and replayer.
	class TernSched {
	protected:
		// Any sub class of TernSched is an app-level scheduler, and it should be race-free, so we need this.
		pthread_mutex_t mutex;
		
	public:
		TernSched() {pthread_mutex_init(&mutex, NULL);}
		
		virtual void appStart() = 0;
		virtual void appEnd(int *info) = 0;

		virtual void taskStart(int *winNum, int instId, int hookId, void *addr, unsigned nBytes, const char *symVarName) = 0;
		virtual int taskEnd(int *winNum, int instId, int hookId) = 0;

		virtual void threadCreateStart(unsigned arg) = 0;
		virtual void threadCreateEnd(unsigned arg, int pthreadId) = 0;
		virtual void threadExit(int *info, int hookId, bool realExit = 0) = 0;

		virtual void symbolic(void *addr, unsigned nbytes, const char *name) = 0;

		virtual void beforeLandmark(unsigned arg0, unsigned hook_id, int instId, uint64_t arg1, uint64_t arg2, uint64_t arg3/*, std::string callStackStr*/) = 0;
		virtual void afterLandmark(pthread_t *tid, unsigned arg0, unsigned hook_id, int instId, uint64_t ret_val, uint64_t arg1, uint64_t arg2, uint64_t arg3/*, std::string callStackStr*/) = 0;

		virtual void waitForTurn(const char *landmarkName, unsigned arg, int hookId = -1) = 0;
		virtual void giveUpTurn(const char *landmarkName, unsigned arg) = 0;

		void lock() {pthread_mutex_lock(&mutex);}
		void unLock() {pthread_mutex_unlock(&mutex);}
		pthread_mutex_t *getMutex() {return &mutex;}
	};
}
#endif

